\subsection{Generación de Fórmulas}

\begin{frame}{Generación de Fórmulas}
\tableofcontents[currentsection,currentsubsection]
\end{frame}

\begin{frame}{Generación de Fórmulas}
\begin{block}
\LARGE Representación de la Base de Datos \pause $ \rightarrow $ Fórmulas de las restricciones
\end{block}
\end{frame}


\subsubsection{Introducción}

\begin{frame}{Introducción}
\begin{itemize}
\item Búsqueda de casos de prueba \pause  $ \rightarrow $ resolución de restricciones
\pause \item Instancia simbólica de la base de datos
\pause \item Multiconjunto de Fórmulas y Sustituciones
\end{itemize}
\end{frame}

\subsubsection{Instancia Simbólica}
\begin{frame}[fragile]{Instancia Simbólica}
\begin{itemize}
\item Nombre de la vista a estudiar
\item Número de filas por cada tabla implicada

\end{itemize}
\pause \begin{block}{Tabla notas con 2 filas}
\begin{tabular}{|c|c|}
\hline
\multicolumn{2}{|c|}{\textbf{notas}} \\
\hline
dni & nota\\
\hline
notas.dni.0 & notas.nota.0 \\
notas.dni.1 & notas.nota.1 \\
\hline
\end{tabular}
\end{block}
\end{frame}

\subsubsection{Fórmulas}
\begin{frame}[fragile]{Fórmulas}
 Multiconjunto de pares de 
\begin{itemize}
\item Formulas de primer orden
\item Renombramientos
\end{itemize}
\pause
\begin{columns}
\column{.48\textwidth}
\begin{block}{Renombramiento}

 \begin{verbatim}
aprobados.dni -> notas.dni.0
\end{verbatim}
\end{block}
\column{.48\textwidth}
\begin{block}{Fórmula}
\begin{verbatim}
(notas.dni.0 != notas.dni.1)
AND (notas.nota.0 >= 5)
\end{verbatim}
\end{block}
\end{columns}
\pause
\begin{columns}
\column{.48\textwidth}
\begin{block}{Renombramiento}

 \begin{verbatim}
aprobados.dni -> notas.dni.1
\end{verbatim}
\end{block}
\column{.48\textwidth}
\begin{block}{Fórmula}
\begin{verbatim}
(notas.dni.0 != notas.dni.1)
AND (notas.nota.1 >= 5)
\end{verbatim}
\end{block}
\end{columns}
\end{frame}

